\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Qa}$, ${\it Rb}$, ${\it Sc}$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$, $C$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$),\+
\\[0ex]${\it Ic}$:AbsInterface($C$), $f_{1}$:(E(${\it Ia}$)$\rightarrow$$B$), $f_{2}$:($B$$\rightarrow$$C$).
\-\\[0ex](Q{-}R{-}glued(${\it es}$; $B$; $f_{1}$; ${\it Ia}$; ${\it Qa}$; ${\it Ib}$; ${\it Rb}$) \& Q{-}R{-}glued(${\it es}$; $C$; ($\lambda$$e$.$f_{2}$(${\it Ib}$($e$))); ${\it Ib}$; ${\it Rb}$; ${\it Ic}$; ${\it Sc}$))
\\[0ex]$\Rightarrow$ Q{-}R{-}glued(${\it es}$; $C$; ($f_{2}$ o $f_{1}$); ${\it Ia}$; ${\it Qa}$; ${\it Ic}$; ${\it Sc}$)
\end{tabbing}